\begin{tabbing}
pre{-}init{-}p2(${\it es}$;$i$;${\it ds}$;${\it init}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$P$ holds in state ${\it init}$ $\Rightarrow$ $\exists$e@$i$\+
\\[0ex]\& @$i$ \=Precondition for $a$(v)\+
\\[0ex]$P$ State(${\it ds}$) (v:$T$)
\-\\[0ex]\& ($\forall$$x$:Id. $x$ $\in$ dom(${\it ds}$) $\Rightarrow$ @$i$ $x$ initially ${\it init}$($x$):${\it ds}$($x$))
\-
\end{tabbing}